(* Copyright Per Lindgren 2015, see the file "LICENSE" for the full        *)
(* license governing this code.                                            *)

(* FUN-4SURE/Main *)

open Common
open Options (* to make opt available in scope *)
open Lexing  (* no make lexbuf available in scope *)
open AST
open ST
open Env
open Well
   
let main () =
  (* let t_start = Sys.time() in *)
  Cmd.cmd; (* parse command line options and put into opt *)
  p_stderr (Options.string_of_opt Options.opt);
  let infile = Options.opt.infile in
  p_stderr ("Processing : " ^ infile ^ nl);
  let inBuff =
    try Some (open_in infile)
    with _ -> None
  in
  match inBuff with
  | None          -> p_stderr ("File open error :" ^ infile); raise (RtfmError("Exit"))
  | Some inBuffer -> 
      let lexbuf = Lexing.from_channel inBuffer in
      lexbuf.lex_curr_p <- { lexbuf.lex_curr_p with pos_fname = infile };
      
      try
        let res = Parser.prog Lexer.lex lexbuf in
        match res with
        | None     -> p_stderr ("Not accepted!" ^ nl); raise (RtfmError("Exit"))
        | Some (p) ->
            if Options.opt.verbose then p_stderr ("Parsing of " ^ infile ^ " succeeded:" ^ nl);
            if Options.opt.d_ast then p_stderr (st_of_fbs p);
            
            (* check well formedness *)
            let _ = well p in
            
            
            (* gv_task output *)
            if Options.opt.gv_ecc then begin
              let oc = open_out Options.opt.gv_eccf in
              p_oc oc (Gv.gv_of_fb p);
              close_out oc; 
            end; 
            
            (* WhyML output *)
            if Options.opt.why then begin
              let oc = open_out Options.opt.whyf in
              p_oc oc (WhyML.why_of_fbs p);
              close_out oc; 
            end;
            
            [] (* unit list *)
            
            
      (* exception handling *)
      with
      | Lexer.SyntaxError msg -> p_stderr ("Syntax error." ^ msg ^ Error.parse_err_msg lexbuf) :: []
      | Parser.Error          -> p_stderr ("Parser error." ^ Error.parse_err_msg lexbuf) :: []
      | RtfmError msg         -> p_stderr ("Error : " ^ msg ) :: []  
;;

main ();;
